\begin{tabbing}
$\forall$${\it es}$:ES, $a$:Atom1, $e$:E.
\\[0ex]loc($e$) $\parallel$ $a$
\\[0ex]$\Rightarrow$ \=((\=($\neg$($\uparrow$first($e$)))\+\+
\\[0ex]$\Rightarrow$ (($\uparrow$isrcv(pred($e$))) $\Rightarrow$ val(pred($e$)):valtype(pred($e$))$\parallel$$a$)
\\[0ex]$\Rightarrow$ es\_state\_when(${\it es}$;pred($e$)):es\_state(${\it es}$;loc(pred($e$)))$\parallel$$a$
\\[0ex]$\Rightarrow$ es\_state\_when(${\it es}$;$e$):es\_state(${\it es}$;loc($e$))$\parallel$$a$)
\-\\[0ex]\& (\=(($\uparrow$isrcv($e$)) $\Rightarrow$ val($e$):valtype($e$)$\parallel$$a$)\+
\\[0ex]$\Rightarrow$ es\_state\_when(${\it es}$;$e$):es\_state(${\it es}$;loc($e$))$\parallel$$a$
\\[0ex]$\Rightarrow$ $e$ sends $\parallel$ $a$))
\-\-
\end{tabbing}